sframe-p(es; l; tg; L)
== e:es-E(es). (es-kind(es; e) = rcv(l,tg))  (es-kind(es; es-sender(es; e))  L) 

latex

---

clarification:

sframe-p(es; l; tg; L)
== e:es-E(es). 
== (es-kind(es; e) = rcv(l,tg)  Knd)  (es-kind(es; es-sender(es; e))  L  Knd) 

latex

Definitions	x:A. B(x), es-E(es), P  Q, rcv(l,tg), (x  l), es-kind(es; e), es-sender(es; e), Knd
FDL editor aliases	sframe-p